(declare-fun v4 () Bool)
(declare-fun v7 () Bool)
(declare-fun v8 () Bool)
(declare-fun str0 () String)
(declare-fun str1 () String)
(declare-fun str3 () String)
(declare-fun str4 () String)
(declare-fun str5 () String)
(declare-fun str7 () String)
(assert (and v8 (str.in_re (str.++ str5 str4 str3 str7 str3) (re.+ (str.to_re "rl")))))
(assert (str.contains str0 str5))
(push)
(declare-fun v49 () Bool)
(assert (not (str.in_re str7 (str.to_re str3))))
(assert (and v7 (str.prefixof str1 str3) (= v4 v49)))
(check-sat)
